int_loset()  LOSet{1} 

latex

Up	sets 1
Definitions of Statement	int_loset()
Definitions	int_loset(), t  T, P & Q, x. t(x), P  Q, , P  Q, x f y, P  Q, x:A. B(x), IsEqFun(T;eq), x,y. t(x;y), P  Q, False, A, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), A  B, Linorder(T;x,y.R(x;y)), x(s), x(s1,s2)
Lemmas	le int wf, eq int wf, mk oset wf, assert of eq int, iff functionality wrt iff, assert wf, iff wf, all functionality wrt iff, assert of le int, le wf, linorder functionality wrt iff